$\forall$$A$, $B$:Realizer.
\\[0ex]Rplus?($A$)
\\[0ex]$\Rightarrow$ ($\forall$$i$:Id. R{-}da(Rplus{-}left($A$);$i$) $\parallel$ R{-}da(Rplus{-}right($A$);$i$))
\\[0ex]$\Rightarrow$ (R{-}interface($B$;$A$) $\Leftrightarrow$ R{-}interface($B$;Rplus{-}left($A$)) \& R{-}interface($B$;Rplus{-}right($A$)))